;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Mlist.lisp")
(require "Mtrim.lisp")
(require "Mmerge-sort.lisp")
(require "Mtranspose-fast.lisp")
(require "Mformulas-aux.lisp")
(require "Mschedule-criterion.lisp")
(require "Mgpa-criterion.lisp")
(require "Mgender-criterion.lisp")
(require "Mskill-sets-criterion.lisp")
(require "Mdriver.lisp")
(require "MAVLtree.lisp")
(require "McommonTimes.lisp")
(require "Mformulas.lisp")
(require "Mrng.lisp")

(module TcommonTimes
  (import IAVLtree)
  (import IcommonTimes)
  
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  (include-book "avl-rational-keys" :dir :teachpacks)
  (include-book "list-utilities" :dir :teachpacks)
  
  ;;#####################################################
  ;;Helper Functions
  ;;#####################################################
  (defrandom randomBit()
    (random-between 0 1))
  
  (defrandom randomBits(x)
    (if (> x 0)
        (cons (randomBit) (randomBits (- x 1)))
        nil))
  
  (defrandom randomBitArray ()
    (append (randomBits 335) (list 1)))
  
  (defun countOccurences(target list)
    (if (consp list)
        (if (equal target (car list))
            (+ 1 (countOccurences target (cdr list)))
            (countOccurences target (cdr list)))
        0))
  
;  (defun containsMatchingString(listOfStrings string)
;    (if (consp listOfStrings)
;        (if (equal (car listOfStrings) string)
;            t
;            (containsMatchingString (cdr listOfStrings) string))
;        nil))
;  
;  (defun allStringsHaveMatch(listOfStrings potentialMatches)
;    (if (consp listOfStrings)
;        (if (containsMatchingString (car listOfStrings) potentialMatches)
;            (allStringsHaveMatch (cdr listOfStrings) potentialMatches)
;            nil)
;        t))
  
  
  ;;#####################################################
  ;;Check Expects
  ;;#####################################################
  
  (check-expect "M 5:00pm ~ M 7:00pm; W 6:00pm ~ W 8:00pm; R 1:00pm ~ R 2:00pm"   (bitlist->timesstring '(1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1)))
  (check-expect (timestring->bitlist "M 5:00pm ~ M 7:00pm; W 6:00pm ~ W 8:00pm; R 1:00pm ~ R 2:00pm")   '(1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1)) 
  
  (check-expect  '(1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1)  (timestring->bitlist (bitlist->timesstring '(1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1))))
  (check-expect  '(0 0 1 1 1 1 1 0 1 0 0 1 0 0 1 0 0 1 0 0 1 0 1 0 0 0 1 1 1 1 1 0 0 1 0 0 0 1 1 1 1 1 1 0 1 0 1 1 0 0 1 0 1 1 1 0 1 1 0 0 0 1 1 1 0 0 1 0 1 1 0 1 1 0 1 1 1 0 0 0 1 0 0 0 0 0 1 0 1 0 1 1 1 1 1 0 0 0 1 0 1 1 1 1 0 1 1 0 0 0 0 1 0 0 1 1 1 0 1 0 0 0 0 1 1 1 0 0 0 0 1 1 1 0 0 0 1 1 1 0 0 1 0 1 0 0 1 1 1 1 0 0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 1 0 1 1 0 0 0 0 1 1 1 1 0 1 1 1 1 1 0 1 0 0 0 1 0 0 0 0 0 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 1 0 0 1 1 1 1 1 1 1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 0 1 0 1 0 0 0 1 1 0 0 0 1 0 1 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 1 0 1 0 0 0 0 0 1 1 1 1 1 0 1 1 0 1 0 1 1 0 0 0 0 0 1 0 0 1 0 1 1 0 1 1 0 1 0 0 0 0 1 1 1 1 1 0 0 1)  (timestring->bitlist (bitlist->timesstring '(0 0 1 1 1 1 1 0 1 0 0 1 0 0 1 0 0 1 0 0 1 0 1 0 0 0 1 1 1 1 1 0 0 1 0 0 0 1 1 1 1 1 1 0 1 0 1 1 0 0 1 0 1 1 1 0 1 1 0 0 0 1 1 1 0 0 1 0 1 1 0 1 1 0 1 1 1 0 0 0 1 0 0 0 0 0 1 0 1 0 1 1 1 1 1 0 0 0 1 0 1 1 1 1 0 1 1 0 0 0 0 1 0 0 1 1 1 0 1 0 0 0 0 1 1 1 0 0 0 0 1 1 1 0 0 0 1 1 1 0 0 1 0 1 0 0 1 1 1 1 0 0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 1 0 1 1 0 0 0 0 1 1 1 1 0 1 1 1 1 1 0 1 0 0 0 1 0 0 0 0 0 0 0 1 1 0 0 1 0 0 1 0 1 0 1 1 1 0 0 1 1 1 1 1 1 1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 0 1 0 1 0 0 0 1 1 0 0 0 1 0 1 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 1 1 0 1 0 0 0 0 0 1 1 1 1 1 0 1 1 0 1 0 1 1 0 0 0 0 0 1 0 0 1 0 1 1 0 1 1 0 1 0 0 0 0 1 1 1 1 1 0 0 1))))
  (check-expect  '(1 1 1 0 0 1 1 0 1 1 0 1 0 0 0 0 0 0 0 1 0 1 0 0 0 1 0 0 1 1 0 0 0 1 0 0 0 1 0 1 1 1 1 0 1 1 0 0 1 0 0 1 0 0 0 0 1 0 0 1 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 0 1 0 1 1 0 1 1 1 1 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 1 1 0 0 0 1 1 1 0 1 0 0 1 1 1 1 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 0 0 1 1 0 1 0 0 1 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 0 1 0 0 1 0 0 0 1 0 0 1 1 1 1 1 1 1 0 0 1 1 0 0 1 0 0 0 0 1 0 0 1 0 1 0 0 0 0 1 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 0 1 0 1 1 0 0 1 0 1 1 1 0 0 0 1 0 0 1 0 0 1 1 0 0 1 1 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0 0 0 1 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 0 0 0 1 1 0 0 0 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 1 1 1 0 1 0 0 0 0 0 0 1 1 1)  (timestring->bitlist (bitlist->timesstring '(1 1 1 0 0 1 1 0 1 1 0 1 0 0 0 0 0 0 0 1 0 1 0 0 0 1 0 0 1 1 0 0 0 1 0 0 0 1 0 1 1 1 1 0 1 1 0 0 1 0 0 1 0 0 0 0 1 0 0 1 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 0 1 0 1 1 0 1 1 1 1 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 1 1 0 0 0 1 1 1 0 1 0 0 1 1 1 1 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 0 0 1 1 0 1 0 0 1 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 0 1 0 0 1 0 0 0 1 0 0 1 1 1 1 1 1 1 0 0 1 1 0 0 1 0 0 0 0 1 0 0 1 0 1 0 0 0 0 1 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 0 1 0 1 1 0 0 1 0 1 1 1 0 0 0 1 0 0 1 0 0 1 1 0 0 1 1 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0 0 0 1 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 0 0 0 1 1 0 0 0 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 1 1 1 0 1 0 0 0 0 0 0 1 1 1))))
  (check-expect  '(1 1 0 1 1 0 1 1 0 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 1 0 0 0 0 0 1 1 0 1 0 0 1 1 0 0 0 0 0 1 0 1 1 1 0 1 0 0 1 0 1 0 0 1 0 0 0 0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1 1 1 0 0 1 1 1 0 1 0 1 0 0 0 0 1 1 0 0 0 1 0 1 1 0 1 1 0 1 1 1 0 1 0 1 0 0 1 0 0 1 0 0 0 1 0 0 0 1 1 1 1 1 1 1 1 1 1 0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 0 0 1 1 0 1 0 0 0 1 0 0 1 1 1 0 0 0 0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 0 0 0 0 1 1 1 0 1 0 0 0 1 1 0 0 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 1 0 1 1 1 0 0 0 1 1 1 1 1 0 1 0 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 0 0 0 0 1 0 1 1 1 0 1 1 0 0 0 1 0 1 0 0 1 0 0 1 1 1 0 0 1 1 1 0 0 1 1 0 1 1 0 0 0 0 0 0 1 1 0 1 1 0 1 1 0 1 0 1 1 1 1 0 0 0 0 1)  (timestring->bitlist (bitlist->timesstring '(1 1 0 1 1 0 1 1 0 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 1 0 0 0 0 0 1 1 0 1 0 0 1 1 0 0 0 0 0 1 0 1 1 1 0 1 0 0 1 0 1 0 0 1 0 0 0 0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1 1 1 0 0 1 1 1 0 1 0 1 0 0 0 0 1 1 0 0 0 1 0 1 1 0 1 1 0 1 1 1 0 1 0 1 0 0 1 0 0 1 0 0 0 1 0 0 0 1 1 1 1 1 1 1 1 1 1 0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 0 0 1 1 0 1 0 0 0 1 0 0 1 1 1 0 0 0 0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 0 1 1 0 1 1 0 0 1 0 1 0 1 0 0 0 1 1 0 0 0 0 1 1 1 0 1 0 0 0 1 1 0 0 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 1 0 1 1 1 0 0 0 1 1 1 1 1 0 1 0 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 0 0 0 0 1 0 1 1 1 0 1 1 0 0 0 1 0 1 0 0 1 0 0 1 1 1 0 0 1 1 1 0 0 1 1 0 1 1 0 0 0 0 0 0 1 1 0 1 1 0 1 1 0 1 0 1 1 1 1 0 0 0 0 1))))
  
  
  (check-expect "U 12:00am ~ U 11:00pm" (bitlist->timesstring (timestring->bitlist "U 12:00am ~ U 11:00pm")))
  (check-expect "U 12:00am ~ M 12:00am" (bitlist->timesstring (timestring->bitlist "U 12:00am ~ M 12:00am")))
  (check-expect "U 12:00am ~ S 11:30pm" (bitlist->timesstring (timestring->bitlist "U 12:00am ~ S 11:30pm")))
  (check-expect "U 12:30am ~ U 12:30pm" (bitlist->timesstring (timestring->bitlist "U 12:30am ~ U 12:30pm")))
  
  (check-expect "F 1:00am ~ S 1:00pm; S 5:00pm ~ S 7:30pm" (bitlist->timesstring (timestring->bitlist "F 1:00am ~ S 1:00pm; S 5:00pm ~ S 7:30pm")))
  (check-expect "F 1:00am ~ S 1:00pm; S 5:00pm ~ S 7:30pm" (bitlist->timesstring (timestring->bitlist "S 5:00pm ~ S 7:30pm; F 1:00am ~ S 1:00pm")))
  
                                                                                                       
  ;;#####################################################
  ;;Property Tests
  ;;#####################################################
  (defproperty BitlistTimestringRoundTrip
    (bitArray :value (randomBitArray))
    (equal bitArray (timestring->bitlist (bitlist->timesstring bitArray))))
  
  (defproperty CommonTimesLessThanOriginals
    (bitArray1 :value (randomBitArray)
     bitArray2 :value (randomBitArray))
    (let* ((commonTimes (time-bitwise-and bitArray1 bitArray2))
           (commonZeros (countOccurences 0 commonTimes))
           (time1Zeros  (countOccurences 0 bitArray1))
           (time2Zeros  (countOccurences 0 bitArray2)))
      (and (<= commonZeros time1Zeros) (<= commonZeros time2Zeros))))
  
  
  
  ;Realized that what I was trying to do won't actually work...
;  (defproperty CommonTimesTest
;    (bitArray1 :value (randomBitArray)
;     bitArray2 :value (randomBitArray))
;    (let* ((commonTimes (time-bitwise-and bitArray1 bitArray2))
;           (commonTimesStrings (map-chrs->str (packets #\; (remove #\space (str->chrs (bitlist->timestring commonTimes))))))
;           (time1Strings (map-chrs->str (packets #\; (remove #\space (str->chrs (bitlist->timestring bitArray1))))))
;           (time2Strings (map-chrs->str (packets #\; (remove #\space (str->chrs (bitlist->timestring bitArray2)))))))
;      (and (allStringsHaveMatch commonTimesStrings time1Strings) (allStringsHaveMatch commonTimeStrings
;      
      
  
  
)


(link RTcommonTimes
      (Mlist Mtrim Mmerge-sort Mtranspose-fast Mformulas-aux
         Mschedule-criterion Mgpa-criterion Mgender-criterion Mskill-sets-criterion 
         Mformulas Mrng MAVLtree McommonTimes TcommonTimes)
)


(invoke RTcommonTimes)